\begin{tabbing}
es{-}change{-}to(${\it es}$;$T$;$x$;$e$;$v$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=es{-}dtype(${\it es}$; es{-}loc(${\it es}$; $e$); $x$; $T$)\+
\\[0ex]c$\wedge$ (($\neg$(es{-}when(${\it es}$; $x$; $e$) = $v$ $\in$ $T$)) $\wedge$ (es{-}after(${\it es}$; $x$; $e$) = $v$ $\in$ $T$))
\-
\end{tabbing}